$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), $P$:(($B$ List)$\rightarrow$Prop). safety($B$;$L$.$P$($L$)) $\Rightarrow$ safety($A$;$L$.$P$(map($f$;$L$)))